%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Task
%CreateTask\_T
%DeleteTask\_T
%ExecuteRunningTask\_T
%SuspendTask\_T
%ResumeTask\_T
%ChangeTaskPriority\_T
%Migration\_T
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\documentclass[a4paper, 12pt]{article}

\usepackage[margin=2cm, includeheadfoot]{geometry}
\usepackage{z-eves}

\makeatletter
\renewcommand{\@znoskip}{\offinterlineskip}
\makeatother

\begin{document}

%\begin{zsection}
%  \SECTION m6Task \parents standard\_toolkit
%\end{zsection}

\begin{zed}
  [CONTEXT, TASK, CORE]
\end{zed}

\begin{axdef}
  bare\_context: CONTEXT\\
  idles: \finset TASK\\
  cores: \finset CORE
\where
  \# cores = \# idles\\
  cores \neq \emptyset
\end{axdef}

\begin{zed}
STATE ::= nonexistent | ready | blocked | suspended | running
\end{zed}

\begin{zed}
%\begin[disabled]{zed}
transition == (\{blocked\} \cross  \{nonexistent, ready, running, suspended\})\\
			   \t1 \cup  (\{nonexistent\} \cross  \{ready, running\})\\
			   \t1 \cup  (\{ready\} \cross  \{nonexistent, running, suspended\})\\
			   \t1 \cup  (\{running\} \cross  \{blocked, nonexistent, ready, suspended\})\\
			   \t1 \cup  (\{suspended\} \cross  \{nonexistent, ready, running\})
\end{zed}

\begin{axdef}
  slice\_delay: \nat 
\where
%  \Label{disabled slice_delay_def} slice\_delay = 1
slice\_delay = 1
\end{axdef}

\begin{schema}{TaskData}
  tasks: \finset  TASK\\
  running\_tasks: cores \inj TASK\\
  executable: TASK \psurj cores
\where
  \ran running\_tasks \subseteq  tasks\\
  idles \subseteq  tasks\\
  \dom executable =  tasks\\
  \forall t: \ran running\_tasks @ running\_tasks \inv t = executable~t
\end{schema}

\begin{schema}{Init\_TaskData}
  TaskData'
\where
  tasks' = idles\\
\end{schema}

\begin{schema}{StateData}
  state: TASK \fun  STATE
\where
  \forall i: idles @ state(i) \in  \{ready, running\}
\end{schema}

\begin{schema}{Init\_StateData}
  StateData'
\where
  state' = (\lambda  x: TASK @ nonexistent) \oplus  (idles \cross \{running\})
\end{schema}

\begin{schema}{ContextData}
  phys\_context: cores \fun CONTEXT\\
  log\_context: TASK \fun  CONTEXT
\end{schema}

\begin{schema}{Init\_ContextData}
  ContextData'
\where
  phys\_context' = (\lambda c: cores @ bare\_context)\\
  log\_context' = (\lambda  x: TASK @ bare\_context)
\end{schema}

\begin{schema}{PrioData}
  priority: TASK \fun  \nat 
\where
  \forall i: idles @ priority(i) = 0
\end{schema}

\begin{schema}{Init\_PrioData}
  PrioData'
\where
  priority' = (\lambda  x: TASK @ 0)
\end{schema}

\begin{schema}{Task}
  TaskData\\
  StateData\\
  ContextData\\
  PrioData
\where
  tasks = TASK \setminus  (state \inv  \limg  \{nonexistent\} \rimg )\\
  state \inv  \limg  \{running\} \rimg  = \ran running\_tasks\\
  \forall  pt: state \inv  \limg  \{ready\} \rimg; r: \ran running\_tasks\\
  		\t1 | executable(pt) = executable(r) @ priority(r) \geq  priority(pt)
\end{schema}

\begin{schema}{\Delta Task}
  Task\\
  Task'
\where
  \forall  st: TASK | state'(st) \neq  state(st) @ state(st) \mapsto  state'(st) \in  transition
\end{schema}

\begin{schema}{Init}
%\begin{schema}{Init\_Task}
  Task'
\where
  Init\_TaskData\\
  Init\_StateData\\
  Init\_ContextData\\
  Init\_PrioData
\end{schema}

\begin{schema}{createTaskSpeCoreN\_T}
  \Delta Task\\
  target?: TASK\\
  newpri?: \nat\\
  executeCore: CORE
\where
  executeCore \in cores\\
  state(target?) = nonexistent\\
  newpri? \leq priority(running\_tasks(executeCore))\\ 
  tasks' = tasks \cup \{target?\}\\
  running\_tasks' = running\_tasks\\
  executable' = executable \oplus \{(target? \mapsto executeCore)\}\\
  state' = state \oplus \{(target? \mapsto ready)\}\\
  \Xi ContextData\\
  priority' = priority \oplus \{(target? \mapsto newpri?)\}
\end{schema}

\begin{schema}{findACore\_T}
  Task\\
  target?: TASK\\
  newpri?: \nat\\
  executeCore?: CORE\\
  executeCore: CORE
\where
  executeCore? \notin cores\\
  executeCore \in cores\\
  \exists tcs, cs: \finset cores |\\
  \t1 tcs = \{~pc: cores | newpri? > priority(running\_tasks(pc))~\}\\
  \t1 @ (tcs = \emptyset \implies cs = cores) \land (tcs \neq \emptyset \implies cs = tcs)\\
  \t2    \land (\forall oc: cs @ executeCore \in cs\\
  \t3        \land \# (executable \inv \limg\{executeCore\}\rimg) \leq \# (executable \inv \limg\{oc\}\rimg))
\end{schema}

\begin{zed}
  CreateTaskN\_T \defs ([executeCore?, executeCore: CORE\\
  \t1	 | executeCore? \in cores \land executeCore = executeCore?] \lor findACore\_T)\\
  \t1  \land createTaskSpeCoreN\_T
\end{zed}

\begin{schema}{Reschedule}
  \Delta Task\\
  target?: TASK\\
  tasks?: \finset  TASK\\
  executable?: TASK \psurj cores\\
  st?: STATE\\
  pri?: TASK \fun  \nat
\where
  tasks' = tasks?\\
  running\_tasks' = running\_tasks \oplus \{(executable?(target?) \mapsto target?)\}\\
  executable' = executable?\\%executable \oplus \{(target? \mapsto executeCore?)\}\\
  state' = state \oplus  \{(target? \mapsto  running),\\
  	\t1 (running\_tasks(executable?(target?)) \mapsto  st?)\}\\
  phys\_context' = phys\_context \oplus \{(executable?(target?) \mapsto log\_context(target?))\}\\
  log\_context' = log\_context \oplus\\
  \t1	\{(running\_tasks(executable?(target?))\\
  \t2     \mapsto  phys\_context(executable?(target?)))\}\\
  priority' = pri?
\end{schema}

\begin{zed}
  disableReschedule \defs  [Task|false] \land Reschedule
\end{zed}

\begin{schema}{createTaskSpeCoreS\_T}
  \Delta Task\\
  target?: TASK\\
  newpri?: \nat\\
  executeCore: CORE	
\where
  executeCore \in cores\\
  state(target?) = nonexistent\\
  newpri? > priority(running\_tasks(executeCore))\\ 
  \exists st?: STATE; tasks?: \finset TASK; executable?: TASK \psurj cores;\\
  \t1 pri?: TASK \fun \nat\\
  \t1 | st? = ready \land tasks? = tasks \cup \{target?\}\\
  \t1 \land executable? = executable \oplus \{(target? \mapsto executeCore)\}\\
  \t1 \land pri? = priority \oplus \{(target? \mapsto newpri?)\} @ Reschedule
\end{schema}

\begin{zed}
  CreateTaskS\_T \defs ([executeCore?, executeCore: CORE\\
  	\t1 | executeCore? \in cores \land executeCore = executeCore?]  \lor findACore\_T)\\
  	\t1 \land createTaskSpeCoreS\_T
\end{zed}

\begin{zed}
  CreateTask\_T \defs CreateTaskN\_T \lor CreateTaskS\_T
\end{zed}

\begin{schema}{DeleteTaskN\_T}
  \Delta Task\\
  target?: TASK\\
  topReady!: TASK
\where
  target? \in tasks \setminus idles\\
  state(target?) \in \{ready, blocked, suspended\}\\
  tasks' = tasks \setminus \{target?\}\\
  running\_tasks' = running\_tasks\\
  executable' = \{target?\} \ndres executable\\
  state' = state \oplus \{(target? \mapsto nonexistent)\}\\
  phys\_context' = phys\_context\\
  log\_context' = log\_context \oplus \{(target? \mapsto bare\_context)\}\\
  \Xi PrioData\\
  topReady! = running\_tasks(executable(target?))
\end{schema}

\begin{schema}{findTopReady}
  Task\\
  target?: TASK\\
  topReady!: TASK
\where
  state(topReady!) = ready\\
  executable(topReady!) = executable(target?)\\
  \forall rt: state \inv \limg \{ready\} \rimg | executable(rt) = executable(topReady!)\\
  \t1 @ priority(topReady!) \geq priority(rt)
\end{schema}

\begin{schema}{DeleteTaskS\_T}
  \Delta Task\\
  target?: TASK\\
  topReady!: TASK
\where
  target? \in tasks \setminus idles\\
  state(target?) = running\\
  findTopReady\\
  tasks' = tasks \setminus \{target?\}\\
  running\_tasks' = running\_tasks \oplus \{executable(target?) \mapsto topReady!\}\\
  executable' = \{target?\} \ndres executable\\
  state' = state \oplus \{(topReady! \mapsto running), (target? \mapsto nonexistent)\}\\
  phys\_context' = phys\_context \oplus\\
  \t1 \{(executable(target?) \mapsto log\_context(topReady!))\}\\
  log\_context' = log\_context \oplus \{(target? \mapsto bare\_context)\}\\
  \Xi PrioData
\end{schema}

\begin{zed}
  DeleteTask\_T \defs DeleteTaskN\_T \lor DeleteTaskS\_T
\end{zed}

\begin{schema}{ExecuteRunningTask\_T}
  \Delta Task\\
  target!: \finset TASK
\where
  \Xi TaskData\\
  \Xi StateData\\
  \forall c: cores @ phys\_context'(c) \neq phys\_context(c)\\
  log\_context' = log\_context\\
  \Xi PrioData\\
  target! = \ran running\_tasks
\end{schema}

\begin{schema}{SuspendTaskN\_T}%suspend task normal case
  \Delta Task\\
  target?: TASK\\
  topReady!: TASK
\where
  state(target?) \in \{ready, blocked\}\\
  target? \notin idles\\
  \Xi TaskData\\
  state' = state \oplus \{(target? \mapsto suspended)\}\\
  \Xi ContextData\\
  \Xi PrioData\\
  topReady! = running\_tasks(executable(target?))
\end{schema}

\begin{schema}{SuspendTaskS\_T}%suspend task schedule case, i.e. suspend running task
  \Delta Task\\
  target?: TASK\\
  topReady!: TASK
\where
  state(target?) = running\\
  target? \notin idles\\
  findTopReady\\
  \exists st?: STATE | st? = suspended\\
  \t1 @ Reschedule[tasks/tasks?, executable/executable?, priority/pri?,\\
  \t2        topReady!/target?]
\end{schema}

\begin{schema}{SuspendTaskO\_T}%suspend task other case, i.e. suspend suspended task
  \Xi Task\\
  target?: TASK\\
  topReady!: TASK
\where
  state(target?) = suspended\\
  topReady! = running\_tasks(executable(target?))
\end{schema}

\begin{zed}
  SuspendTask\_T \defs SuspendTaskN\_T \lor SuspendTaskS\_T \lor SuspendTaskO\_T
\end{zed}

\begin{schema}{ResumeTaskN\_T}
  \Delta Task\\
  target?: TASK
\where
  state(target?) = suspended\\
  priority(target?) \leq priority(running\_tasks(executable(target?)))\\
  \Xi TaskData\\
  state' = state \oplus \{(target? \mapsto ready)\}\\
  \Xi ContextData\\
  \Xi PrioData
\end{schema}

\begin{schema}{ResumeTaskS\_T}
  \Delta Task\\
  target?: TASK
\where
  state(target?) = suspended\\
  priority(target?) > priority(running\_tasks(executable(target?)))\\
  \exists st?: STATE | st? = ready\\
  \t1    @ Reschedule[tasks/tasks?, executable/executable?, priority/pri?]
\end{schema}

\begin{zed}
  ResumeTask\_T \defs ResumeTaskN\_T \lor ResumeTaskS\_T
\end{zed}

\begin{schema}{ChangeTaskPriorityN\_T}
  \Delta Task\\
  newpri?: \nat\\
  target?: TASK\\
  topReady!: TASK
\where
  state(target?) = ready \implies newpri? \leq priority(running\_tasks(executable(target?)))\\
  state(target?) = running \implies\\
  \t1 (\forall rt: state \inv \limg \{ready\} \rimg | executable(rt) = executable(target?)\\
  \t1 @ newpri? \geq priority(rt))\\
  state(target?) \neq nonexistent\\
  target? \in idles \implies newpri? = 0\\
  \Xi TaskData\\
  \Xi StateData\\
  \Xi ContextData\\
  priority' = priority \oplus \{(target? \mapsto newpri?)\}\\
  topReady! = running\_tasks(executable(target?))
\end{schema}

\begin{schema}{ChangeTaskPriorityS\_T}
  \Delta Task\\
  newpri?: \nat\\
  target?: TASK\\
  topReady!: TASK
\where
  state(target?) = ready\\
  newpri? > priority(running\_tasks(executable(target?)))\\
  target? \in idles \implies newpri? = 0\\
  \exists st?: STATE; pri?: TASK \fun \nat\\
  \t1 | st? = ready \land pri? = priority \oplus \{(target? \mapsto newpri?)\}\\
  \t1 @ Reschedule[tasks/tasks?, executable/executable?]\\
  topReady! = target?
\end{schema}

\begin{schema}{ChangeTaskPriorityD\_T}
  \Delta Task\\
  newpri?: \nat\\
  target?: TASK\\
  topReady!: TASK
\where
  state(target?) = running\\
  target? \in idles \implies newpri? = 0\\
  findTopReady\\
  newpri? < priority(topReady!)\\
  \exists st?: STATE; pri?: TASK \fun \nat\\
  \t1 | st? = ready \land pri? = priority \oplus \{(target? \mapsto newpri?)\}\\
  \t1 @ Reschedule[tasks/tasks?, executable/executable?, topReady!/target?]
\end{schema}

\begin{zed}
  ChangeTaskPriority\_T \defs ChangeTaskPriorityN\_T\\
  \t2 \lor ChangeTaskPriorityS\_T\\
  \t2 \lor ChangeTaskPriorityD\_T
\end{zed}

\begin{schema}{MigrationN\_T}
  \Delta Task\\
  target?: TASK\\
  topReady!: TASK\\
  newCore?: cores
\where
  state(target?) \in \{ready, blocked, suspended\}\\
  state(target?) = ready \implies\\
  \t1 priority(target?) \leq priority(running\_tasks(newCore?))\\
  target? \notin idles\\
  newCore? \neq executable(target?)\\
  tasks' = tasks\\
  running\_tasks' = running\_tasks\\
  executable' = executable \oplus \{(target? \mapsto newCore?)\}\\
  \Xi StateData\\
  \Xi ContextData\\
  \Xi PrioData\\
  topReady! = running\_tasks(newCore?)
\end{schema}

\begin{schema}{MigrationS\_T}%Ready Schedule
  \Delta Task\\
  target?: TASK\\
  topReady!: TASK\\
  newCore?: cores
\where
  state(target?) = ready\\
  priority(target?) > priority(running\_tasks(newCore?))\\
  target? \notin idles\\
  newCore? \neq executable(target?)\\
  \exists st?: STATE; executable?: TASK \psurj cores\\
  \t1 | st? = ready \land executable? = executable \oplus \{(target? \mapsto newCore?)\}\\
  \t1 @ Reschedule[tasks/tasks?, priority/pri?]\\
  topReady! = target?
\end{schema}

\begin{schema}{MigrationRuN\_T}%Runing Normal
  \Delta Task\\
  target?: TASK\\
  topReady!: TASK\\
  newCore?: cores
\where
  state(target?) = running\\
  priority(target?) \leq priority(running\_tasks(newCore?))\\
  target? \notin idles\\
  newCore? \neq executable(target?)\\
  findTopReady\\
  \exists st?: STATE; executable?: TASK \psurj cores\\
  \t1 | st? = ready \land executable? = executable \oplus \{(target? \mapsto newCore?)\}\\
  \t1 @ Reschedule[tasks/tasks?, priority/pri?, topReady!/target?]\\
\end{schema}

\begin{schema}{MigrationRuS\_T}%Running Schedule
  \Delta Task\\
  target?: TASK\\
  topReady!: TASK\\
  newCore?: cores
\where
  state(target?) = running\\
  priority(target?) > priority(running\_tasks(newCore?))\\
  target? \notin idles\\
  newCore? \neq executable(target?)\\
  findTopReady\\
  tasks' = tasks\\
  running\_tasks' = running\_tasks\\
  \t1 \oplus \{(executable(target?) \mapsto topReady!), (newCore? \mapsto target?)\}\\
  executable' = executable \oplus \{(target? \mapsto newCore?)\}\\
  state' = state\\
  \t1 \oplus \{(topReady! \mapsto running), (running\_tasks(newCore?) \mapsto ready)\}\\
  phys\_context' = phys\_context\\
  \t1 \oplus \{(executable(topReady!) \mapsto log\_context(topReady!)),\\
  \t1 (newCore? \mapsto phys\_context(executable(topReady!)))\}\\
  log\_context' = log\_context\\
  \t1 \oplus \{(running\_tasks(newCore?) \mapsto phys\_context(newCore?))\}\\
  priority' = priority
\end{schema}

\begin{zed}
  Migration\_T \defs MigrationN\_T \lor MigrationS\_T\\
  \t3            \lor MigrationRuN\_T \lor MigrationRuS\_T
\end{zed}

\end{document}
